(declare-const fpv3 Float32)
(declare-const fpv4 Float32)
(declare-const v0 Bool)
(declare-const v2 Bool)
(declare-const v1 Bool)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const v10 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v16 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r7 Real)
(declare-const v18 Bool)
(assert v5)
(declare-const fpv5 Float32)
(declare-const fpv6 Float32)
(push)
(declare-const v19 Bool)
(declare-const fpv7 Float32)
(assert (and (xor v18 (fp.gt fpv5 fpv6 ((_ to_fp 8 24) RNA 0.3777009132) ((_ to_fp 8 24) RNA 0.3777009132)) v19 v8 (fp.geq (fp.div RNA fpv3 ((_ to_fp 8 24) RTN 732517.0)) (fp.abs fpv4) ((_ to_fp 8 24) RNA 0.3777009132) (fp.abs fpv4))) v13 v0 v16 v19 (fp.lt fpv4 fpv3 ((_ to_fp 8 24) RNA 0.3777009132) ((_ to_fp 8 24) RTN 732517.0)) v14 (fp.lt (fp.abs fpv5) (fp.abs fpv5) fpv7 (fp.abs fpv5) fpv4) v13))
(push)
(assert (and v5 (> r7 0.5866255) (>= 0.0 r1)))
(check-sat)
(pop)
(assert (not (distinct v10 v13 (> r7 0.5866255))))
(check-sat)
